a:Id, T:Top, ds:x:Id fp Type, P:Top, init:x:Id fp ds(x)?Void, x:Id, t:Type, v:t.
ds || x : t
 (x  dom(init)  init(x) = v)
 (x : t initially x = v ||+ with ds: ds init: initaction a:T precondition a(v) is P) 

latex

Definitions

x:A. B(x), Top, a:A fp B(a), f(x)?z, P  Q, f || g, x : v, b, x  dom(f), f(x), A ||+ B, x : t initially x = v, with ds: ds init: initaction a:T precondition a(v) is P, P & Q, M1 || M2, ma-frame-compatible(A;B), mk-ma, , M1 ||decl M2, 1of(t), 2of(t), Prop, deq-member(eq;x;L), reduce(f;k;as), false, Y, if b t else f fi, True, t  T, P  Q, P  Q, P  Q, x. t(x), true, b, T, ma-frame-compat(A;B), xdom(f). v=f(x)   P(x;v), M.rframe(A.pre p for a), M.frame(k affects x), M.aframe(k affects x), M.rframe(A.effect f of k on y), M.sframe(k sends <l,tg>), M.bframe(k sends on l), M.rframe(A.sends tfL of k on l), z != f(x)  P(a;z), False, , x(s), Unit, A, , a = b

Lemmas

assert wf, deq-member wf, assert of bor, eqof wf, bfalse wf, deq property, fpf-dom wf, fpf-trivial-subtype-top, fpf-cap wf, fpf-join-cap-sq, l member wf, bor wf, bool wf, iff transitivity, false wf, eqtt to assert, band wf, bnot wf, btrue wf, not wf, true wf, eqff to assert, bnot thru bor, assert of band, and functionality wrt iff, assert of bnot, assert-eq-id, fpf-ap wf, eq id wf, or functionality wrt iff, Id wf, id-deq wf, fpf-single-dom, fpf-ap-single, fpf-compatible wf, fpf-single wf, fpf wf, top wf